#pragma once

#include <stack>
#include <math.h>
#include <stdexcept>
#include <algorithm>
#include <set>
#include <queue>
#include "IGraph.h"

using namespace std;

typedef enum {
	WHITE = 0,
	GREY,
	BLACK,
} colour;

class Visitor {
public:
	virtual ~Visitor() {};
	virtual void comeToVertex(int Vertex) = 0;
	virtual void leaveVertex(int Vertex) = 0;
	virtual void processEdge(int vertexFrom, int vertexTo) = 0;
};

template <class Visitor> void DFS(const IGraph& graph, Visitor& visitor) {
	vector<bool> visited(graph.getNumberOfVertices(), false);
	for (int vertex = 0; vertex < graph.getNumberOfVertices(); ++vertex) {
		if (!visited[vertex])
			DFSImplementation(graph, visitor, visited, vertex);
	}
}

template <class Visitor> void DFSImplementation(const IGraph& graph, Visitor& visitor, vector<bool>& visited, int vertexStart) {
	stack<int> verticesStack;
	verticesStack.push(vertexStart);
	while (!verticesStack.empty()) {
		int currentVertex = verticesStack.top();

		if (!visited[currentVertex]) {
			visited[currentVertex] = true;
			visitor.comeToVertex(currentVertex);

			vector<int> incidenceList = graph.getIncidenceList(currentVertex);

			for (size_t index = 0; index < incidenceList.size(); ++index) {
				int nextIncidentVertex = incidenceList[index];
				visitor.processEdge(currentVertex, nextIncidentVertex);
				if (!visited[nextIncidentVertex]) {
					verticesStack.push(nextIncidentVertex);
				}
			}
		}
		else {
			visitor.leaveVertex(currentVertex);
			verticesStack.pop();
		}
	}
}

template <class Visitor> void BFS(const IGraph& graph, Visitor& visitor, int vertexStart){
	int verticesNumber = graph.getNumberOfVertices();
	queue<int> verticesQueue;
	vector<bool> visited(verticesNumber, false);
	verticesQueue.push(vertexStart);
	visited[vertexStart] = true;
	visitor.comeToVertex(vertexStart);

	while (!verticesQueue.empty()){
		int currentVertex = verticesQueue.front();
		verticesQueue.pop();

		vector<int> incidenceList = graph.getIncidenceList(currentVertex);

		for (auto &incidentVertex : incidenceList)
		if (!visited[incidentVertex]) {
			visited[incidentVertex] = true;
			visitor.processEdge(currentVertex, incidentVertex);
			visitor.comeToVertex(incidentVertex);
			verticesQueue.push(incidentVertex);
		}
		visitor.leaveVertex(currentVertex);
	}
}

class TopologicalSort {
public:
	TopologicalSort(int verticesNumber) : vertexColour(verticesNumber, WHITE), hasCycle_(false) {}

	void comeToVertex(int vertex) {
		vertexColour[vertex] = GREY;
	}

	void processEdge(int vertexFrom, int vertexTo) {
		if (vertexColour[vertexTo] == GREY) {
			hasCycle_ = true;
			}
	}

	void leaveVertex(int vertex) {
		if (vertexColour[vertex] == BLACK) 
			return;
		vertexColour[vertex] = BLACK;
		reversedTopologicalOrder_.push_back(vertex);
	}

	bool hasCycle() {
		return hasCycle_;
	}

	vector<int> getTopologicalOrder() const {
		vector<int> topologicalOrder(reversedTopologicalOrder_.begin(), reversedTopologicalOrder_.end());
		reverse(topologicalOrder.begin(), topologicalOrder.end());
		return topologicalOrder;
	}

private:
	vector<int> reversedTopologicalOrder_;
	vector<colour> vertexColour;
	bool hasCycle_;
};

pair<bool, vector<int> > getTopologicalOrder(const IGraph& graph) {
	TopologicalSort topologicalSort(graph.getNumberOfVertices());
	DFS(graph, topologicalSort);
	bool success = !topologicalSort.hasCycle();
	return make_pair(success, topologicalSort.getTopologicalOrder());
}

class Tarjan {
public:
	Tarjan(int verticesNumber) : vertexParent_(verticesNumber), time_(0), isComponentRoot_(verticesNumber, true),
		vertexColour(verticesNumber, WHITE), vertextime_(verticesNumber, 0),
		componentOfVertex_(verticesNumber, -1) {}

	void comeToVertex(int vertex) {
		vertextime_[vertex] = ++time_;
		verticesStack_.push(vertex);
		vertexColour[vertex] = GREY;
	}

	void processEdge(int vertex, int incidentVertex) {
		if (vertexColour[incidentVertex] == GREY) {
			if (incidentVertex == vertex) 
				return;
			vertextime_[vertex] = min(vertextime_[incidentVertex], vertextime_[vertex]);
			isComponentRoot_[vertex] = false;
		}

		if (vertexColour[incidentVertex] == WHITE) {
			vertexParent_[incidentVertex] = vertex;
		}

		if (vertexColour[incidentVertex] == BLACK) {
			if (componentOfVertex_[incidentVertex] != -1 || vertextime_[vertex] <= vertextime_[incidentVertex]) 
				return;

			vertextime_[vertex] = vertextime_[incidentVertex];
			isComponentRoot_[vertex] = false;
		}
	}

	void leaveVertex(int vertex) {
		if (vertexColour[vertex] == BLACK) 
			return;

		vertexColour[vertex] = BLACK;
		if (vertextime_[vertexParent_[vertex]] > vertextime_[vertex]) {
			vertextime_[vertexParent_[vertex]] = vertextime_[vertex];
			isComponentRoot_[vertexParent_[vertex]] = false;
		}

		if (isComponentRoot_[vertex]) {
			NewComponent(vertex);
		}
	}

	vector< set<int> > getComponents() const {
		return components_;
	}

	vector<int> getComponentNumbers() const {
		return componentOfVertex_;
	}

private:
	int time_;
	vector<colour> vertexColour;
	vector< set<int> > components_;
	stack<int> verticesStack_;
	vector<int> vertextime_;
	vector<int> vertexParent_;
	vector<bool> isComponentRoot_;
	vector<int> componentOfVertex_;

	void NewComponent(int vertex) {
		set<int> newComponent;
		int currentVertex;

		while (true) {
			currentVertex = verticesStack_.top();
			verticesStack_.pop();
			componentOfVertex_[currentVertex] = (int)components_.size();
			newComponent.insert(currentVertex);
			if (currentVertex == vertex) {
				break;
			}
		}
		components_.push_back(newComponent);
	}
};

vector< set<int> > getComponents(const IGraph& graph) {
	Tarjan tarjan(graph.getNumberOfVertices());
	DFS(graph, tarjan);
	return tarjan.getComponents();
}

inline unique_ptr<IGraph> getCondensationGraph(const IGraph& graph) {
	int verticesNumber = graph.getNumberOfVertices();
	Tarjan tarjan(verticesNumber);
	DFS(graph, tarjan);
	vector<int> componentOfVertex = tarjan.getComponentNumbers();
	vector< set<int> > components = tarjan.getComponents();
	
	set<Edge> setOfCondensationGraphEdges;
	for (int vertex = 0; vertex < verticesNumber; ++vertex) {
		vector<int> incidenceList = graph.getIncidenceList(vertex);
		for (size_t i = 0; i < incidenceList.size(); ++i) {
			if (incidenceList[i] == vertex)
				continue;
			if (componentOfVertex[incidenceList[i]] != componentOfVertex[vertex]) {
				setOfCondensationGraphEdges.insert(Edge(componentOfVertex[vertex], componentOfVertex[incidenceList[i]]));
			}
		}
	}
	vector<Edge> listOfCondensationGraphEdges(setOfCondensationGraphEdges.begin(), setOfCondensationGraphEdges.end());
	return makeCompactGraph(listOfCondensationGraphEdges, components.size());
}

struct Disjunction {
	int firstVariable_;
	int secondVariable_;
	bool negationFirst_;
	bool negationSecond_;

	Disjunction(int firstVariable, int secondVariable, bool negationFirst, bool negationSecond) :
		firstVariable_(firstVariable), secondVariable_(secondVariable), negationFirst_(negationFirst), negationSecond_(negationSecond) {}
};

inline unique_ptr<IGraph> getGraphForTwoSAT(const vector<Disjunction>& disjunctions, int variablesNumber) {
	vector<Edge> edgesList;
	// let vertex 2*n corresponds to variable n, 2*n+1 to its negation
	// so nagation in terms of vertices is equivalent to x^1

	for (size_t i = 0; i < disjunctions.size(); ++i) {
		int firstVertexNumber = 2 * disjunctions[i].firstVariable_ + (disjunctions[i].negationFirst_ ? 1 : 0);
		int secondVertexNumber = 2 * disjunctions[i].secondVariable_ + (disjunctions[i].negationSecond_ ? 1 : 0);
		// a || b is equivalent to (!a => b) && (!b => a)
		edgesList.push_back(Edge((firstVertexNumber ^ 1), secondVertexNumber));
		edgesList.push_back(Edge((secondVertexNumber ^ 1), firstVertexNumber));
	}
	return makeCompactGraph(edgesList, 2 * variablesNumber);
}

inline pair<bool, vector<bool> > twoSAT(const vector<Disjunction>& disjunctions, int variablesNumber) {
	auto graph = getGraphForTwoSAT(disjunctions, variablesNumber);
	Tarjan tarjan(2 * variablesNumber);
	DFS(*graph, tarjan);
	vector<int> componentOfVertex = tarjan.getComponentNumbers();

	vector<bool> result(variablesNumber);

	for (int variableIndex = 0; variableIndex < variablesNumber; ++variableIndex) {
		if (componentOfVertex[2 * variableIndex] == componentOfVertex[2 * variableIndex + 1]) {
			return make_pair(false, result);
		}

		if (componentOfVertex[2 * variableIndex] > componentOfVertex[2 * variableIndex + 1]) {
			result[variableIndex] = false;
		}
		else {
			result[variableIndex] = true;
		}
	}

	return make_pair(true, result);
}